\begin{tabbing} $\forall$\=$k$:Knd, $l$:IdLnk, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$a$:Knd fp$\rightarrow$ Type,\+ \\[0ex]$f$:(${\it tg}$:Id$\times$(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$(${\it da}$(rcv($l$,${\it tg}$))?Void List))) List. \-\\[0ex]with declarations ds:${\it ds}$da:${\it da}$$k$(v) sends $f$ s v on link $l$ $\in$ MsgA \end{tabbing}